D. Shamkanov; 2018; "Circular Proofs for the Gödel-Löb Provability Logic"
メモ
キーワード
メモ
$ \mathfrak{S}_\mathsf{GL} \vdash \Gamma \iff \mathfrak{S}^\mathrm{circ}_\mathsf{K4} \vdash \Gamma
memo
この論文では$ \impliesの方向だけが示されている．
もっと大雑把に言えば，
このSect3の序文を読み取ると書いてあるが，論文では明確にこの形では書いていない．
proof: $ \impliesのみ
Hilbert流演繹体系のために，シーケント$ \Gammaに対して$ \Gamma^\sharp := \bigvee_{\gamma \in \Gamma} \gammaとする． 1. $ \mathfrak{S}^\mathrm{circ}_\mathsf{K4}では様相論理の公理Lを証明することができる．Fig1 https://gyazo.com/1b5e2ed30ab17764855e5fd550dc0631
2. $ \mathsf{GL}のHilbert流演繹体系とシークエント計算体系の証明能力の等価性$ \mathfrak{H}_\mathsf{GL} \vdash \Gamma^\sharp \iff \mathfrak{S}_\mathsf{GL} \vdash \Gamma 3. $ \mathfrak{H}_\mathsf{GL}の公理$ \bf L以外の残りの部分（すなわち$ \sf \mathfrak{H}_K）は$ \mathfrak{S}_\mathsf{K4}で十分にエミュレート可能．
$ \mathfrak{S}_\mathsf{K4} \vdash \Gamma \impliedby \mathfrak{H}_\mathsf{K} \vdash \Gamma^\sharp
当然これは循環証明体系に拡張しても成り立つ．$ \mathfrak{S}^\mathrm{circ}_\mathsf{K4} \vdash \Gamma \impliedby \mathfrak{H}_\mathsf{K} \vdash \Gamma^\sharp
1~3の事実を合わせると
$ \mathfrak{S}_\mathsf{GL} \vdash \Gamma \iff \mathfrak{H}_\mathsf{GL} \vdash \Gamma^\sharp \implies \mathfrak{S}^\mathrm{circ}_\mathsf{K4} \vdash \Gammaとなるから$ \mathfrak{S}_\mathsf{GL} \vdash \Gamma \implies \mathfrak{S}^\mathrm{circ}_\mathsf{K4} \vdash \Gamma．❏ memo
すなわち$ \mathfrak{S}^\mathrm{circ}_\mathsf{\Lambda} \vdash \Gamma \implies \mathfrak{S}_\mathsf{\Lambda'} \vdash \Gamma
Memo: Sect.4